*****∀E walk home,desk,car,S0;

1 (walkable(home)∧((att(desk,home)∨at(desk,home,S0))∧((att(car,home)∨at(car,home,S0))∧at(I,desk,S0))))⊃(at(I,car%
,walk(car,S0))∧∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡at(x,y,S0))))  

*****∀E drive county,home,airport,walk(car,S0);

2 (drivable(county)∧(att(home,county)∧(att(airport,county)∧(at(car,home,walk(car,S0))∧at(I,car,walk(car,S0))))))%
⊃(at(car,airport,drive(airport,walk(car,S0)))∧∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airpor%
t,walk(car,S0)))≡at(x,y,walk(car,S0)))))  

*****∀E attrans1 I,car,airport,drive(airport,walk(car,S0));

3 ((att(I,car)∨at(I,car,drive(airport,walk(car,S0))))∧(att(car,airport)∨at(car,airport,drive(airport,walk(car,S0%
)))))⊃at(I,airport,drive(airport,walk(car,S0)))  

*****TAUTEQ ∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡at(x,y,S0))) walkable,at1,at2,at3,1;

4 ∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡at(x,y,S0)))  

*****∀E ↑ car,home;

5 ¬(car=I)⊃(at(car,home,walk(car,S0))≡at(car,home,S0))  

*****TAUTEQ ∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airport,walk(car,S0)))≡at(x,y,walk(car,S%
0)))) drivable,at4,at5,at3,notI,walkable,at1,at2,1:2,5;

6 ∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airport,walk(car,S0)))≡at(x,y,walk(car,S0))))  

*****∀E ↑ I,car;

7 (¬(I=car∨at(I,car,walk(car,S0)))∨car=car)⊃(at(I,car,drive(airport,walk(car,S0)))≡at(I,car,walk(car,S0)))  

*****TAUTEQ at(I,airport,drive(airport,walk(car,S0))) at1,at2,at3,at4,at5,notI,drivable,walkable,1:7;

8 at(I,airport,drive(airport,walk(car,S0)))